\begin{tabbing}
recognizer(${\it es}$;$i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(@$i$($x$:$\mathbb{B}$) \& (state@$i$ $\subseteq$r State(${\it ds}$)) \& (kindtype($i$;$k$) $\subseteq$r $T$))\+
\\[0ex]c$\wedge$ \=(\=$\forall$$e$@$i$.\+\+
\\[0ex]($\uparrow$($x$ after $e$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. ((${\it e'}$ $\leq$loc $e$  \& kind(${\it e'}$) = $k$) c$\wedge$ ($\uparrow$(${\it test}$((state when ${\it e'}$),val(${\it e'}$))))))
\-\\[0ex]\& $x$ initially@$i$  = ff)
\-\-
\end{tabbing}